T:(IdType), tab:secret-table(T), x:Atom1. st-lookup(tab;x)  (+Atom1)data(T)+Unit 

latex

Definitions

{x:A| B(x) }, , t  T, x:AB(x), x:A. B(x), a<b, #$n, AB, x:AB(x), P & Q, i  j < k, mu(f), P  Q, False, A, , True, T, Void, {i..j}, Unit, f(a), Atom$n, data(T), left+right, Type, x.A(x), x. t(x), 2of(t), inl(x), , inr(x), ij, i<j, p  q, if b t else f fi, let x = a in b(x), b, x:A. B(x), 1of(t), eq_atom$n(x;y), s = t, st-lookup(tab;x), secret-table(T), Id, true, , Prop, b, P  Q, P  Q, P  Q, false, p  q

Lemmas

assert of bor, or functionality wrt iff, bnot thru bor, assert of band, and functionality wrt iff, bfalse wf, band wf, bnot of lt int, eqtt to assert, assert of le int, iff transitivity, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, bnot wf, assert wf, bool wf, btrue wf, secret-table wf, Id wf, mu wf, eq atom wf1, pi1 wf, let wf, ifthenelse wf, bor wf, lt int wf, le int wf, it wf, pi2 wf, data wf, unit wf, nat wf, le wf